$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $x$:$A$, $v$, $P$:Top. ($z$ != $x$ : $v$($x$) $\Rightarrow$ $P$($a$,$z$)) $\sim$ (True $\Rightarrow$ $P$($x$,$v$))